Nuprl Lemma : qbetween_wf
11,40
postcript
pdf
a
,
b
,
c
:
.
a
b
c
latex
Definitions
P
&
Q
,
a
b
c
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
,
qle
wf
origin
a, b, c:
. a 
b c 
a, b, c:. a b c b c Tx:A. B(x)